\section{Objectives \& Scope}
\label{sec:ObjectivesScope}

\subsection{Motivation}
\label{sec:Motivation}

If we generically consider a model transformation as an algorithm describing specific model manipulations, then testing it or proving some of its properties can be envisaged.
However, unlike reactive systems --- for which many verification techniques have been proposed --- a model transformation performs particular computations where:
\begin{itemize}
	\item it typically operates on models, thus on data at a high-level of abstraction rich in semantics and
   \item from a pragmatic point of view, often only the initial input and the final output is of interest and none of the intermediate steps matters.
\end{itemize}
These are primary fundamental differences between model transformations verification and classical verification of programs written in general-purpose programming languages.
Furthermore, model transformations are used to perform specific \MDD computations, such as model refinement, refactoring, translation, synthesis, simulation, or synchronization~\cite{AMT2012,Mens2006}, and \VOLT will focus on the specifics of the formal verification linked to these \MDD activities.

\subsection{Objectives}
\label{sec:Objectives}

To discuss these problems, we would like to invite submissions related to the following topics:
%
\begin{itemize}
   \item Application of formal verification (e.g., theorem proving, model-checking or abstract interpretations) to model transformations:
   \begin{itemize}
      \item Verification of model transformations expressed in languages such as \textsc{Atl}, \textsc{Qvt}, \textsc{Jtl}, \textsc{Tgg}, \textsc{Viatra}, Kermeta, Epsilon, etc.;
      \item Verification of Domain-Specific Model Transformations \cite{Kuhne2010}, in contrast to general-purpose transformations;
      \item Verification techniques dedicated to model transformation;
   \end{itemize}
   \item Taxonomies of techniques for model transformation verification:
   \begin{itemize}
      \item Properties relevant to techniques for model transformation verification;
      \item Reviews and surveys on the practice of verification for model transformations;
   \end{itemize}
   \item Comparisons between formal verification techniques for model transformation versus general-purpose programming languages;
  \item Case studies, comparisons, and experience reports;
  \item Tools and automation.
\end{itemize}

Because verification of model transformations is a challenging topic in terms of application domains, scalability, and industrial acceptance, one of the primary goal for the workshop success is the quality of the discussion and cross-fertilisation between industrial practices and academic research. After three sessions, and a significant number of contributions in the domain (see e.g. \cite{J:Rahim-Whittle:2013,JoT2014} for an overview and survey of the domain), the community has reached the maturity for tackling reasonably expressive transformations. Consequently, and to respond to the workshop annual theme, we would to propose a specific challenge for this edition by calling contributions that allow the verification of three different transformations asking for increasingly difficult verification tasks\footnote{In the vocabulary of \cite{J:Amrani-etAl:2014}, the first transformation is a purely structural translation (aka. \emph{structural bridge}); the second is an operational semantics of a \textsc{Dsl} (aka. \emph{simulation}); and the last one is a translational semantics (aka. \emph{translation with execution delegation}). We will make these transformations together with their correctness properties available on a \textsc{Share} repository after the Proposal's acceptation.}.

We hope in this way to stimulate the community towards concrete, reproducible results as well as a first-level comparison of tools and techniques for model transformation verification.


\subsection{Intended Audience}
\label{sec:IntendedAudience}

\VOLT is open for all practitioners in MDE, from academia or industry who are interested in discussing techniques on the verification and validation of model transfomations. We believe that \STAF provides an ideal federation of conferences (\textsc{Ecmfa}, \textsc{Icmt}, \textsc{Icgt}, and \textsc{Tap}) for providing a well-balanced mix of \VOLT participants.


\subsection{Relevance}
\label{sec:Relevance}

Many members of the \STAF community are of course practitioners of \MDD and have also proposed techniques for \MDD, both for testing and formal verification.
Many software intensive industries (\eg automotive, avionics, telephony) have nowadays standardized the use of \MDD and incorporated the use of models in their development
processes, with a decrease in manufacturing costs (see~\cite{citeulike:9594369} for a well-known example).
Despite interest of the industry in model transformations, the technology is still too academical and not sufficiently standardized.
In particular, studying techniques to raise the level of confidence in a model transformation or ensure that a model transformation is correct in a certain context is certainly the next logical step to raise industrial interest.
Such a study would solidify and promote the whole area of research in model transformation and favor its adoption in real world projects.
Certainly last years' editions were a big success having attracted to the discussions many new participants and stimulated the field of transformation verification by having a dedicated forum.

The specific contribution of \VOLT is to allow an open discussion space that combines solid theoretical work with practical on-the-field experience in verification of model transformations. As such, it represents a valuable and complementary resource for a scientific joint conference like \STAF, especially for participants of \textsc{Ecmfa}, \textsc{Icmt}, and \textsc{Icgt}.


\subsection{Previous Events}
\label{sec:PreviousEvents}

\textsc{VolT} first edition in 2012 was co-located with the International Conference on Software Testing, Verification and Validation (\textsc{Icst}) and organised by Eugene Syriani (who also organise the current one), Levi L\'ucio and Stephan Weissleder. In total, 7 papers were submitted from which 5 were accepted after a thorough peer-review process involving 4 reviewers per paper. A keynote by Pieter Mosterman (Mathworks) preceded the paper presentation: their quality was tremendous and attracted over 30 attendants during the day of the workshop.

\VOLT{} second and third editions in 2013 and 2014 were already co-located with \STAF: they were organised by the same team as the current one (except Leen Lambers).
In 2013, we received 6 papers with 2 accepted for full presentations after a thorough peer-review process involving 3 reviewers per paper and in addition, two submissions have been presented in short talks without publishing the papers to give the authors the possibility to get feedback from the community. There was a keynote presentation given by D\'aniel V\'arro from the Budapest University of Technology and Economics. The event attracted over 20 attendants during the day of the workshop and especially in the afternoon stimulating discussions have been achieved within three different groups.
In 2014, we also received 6 papers and accepted 5 of them after the same review process. The proceedings were published in \textsc{Ceur} \cite{P:VOLT:2014}. Additionally, the organizers and the authors all contributed to a workshop report that summarized the intensive discussion session of the afternoon.

We shall also mention that a special issue in the Journal of Object Technology on \VOLT will be published this year with extended versions of the submitted papers from the first two editions.

This shows that \VOLT's topics interest many researchers. The \STAF community provides interesting contributions to the field of model transformation verification and seems to be a natural forum for \VOLT, because the \STAF community is especially concerned with the specific challenges arising in \MDD and is also covering mostly all of the founders/contributors of/to model transformation approaches. In addition to the interest of the communities attached to the events mentioned earlier, we expect further interest from the International Conference on Tests and Proof (TAP) community that is concerned with the verification of programs that may raise interesting inter-conference discussions. This may be a good opportunity to establish bridges between the different communities working on verification but for different kinds of programs.

In order to increase the visibility of the workshop (and in order to manage potential conflicts of interests), we have a more diversified and extended organization team than for the first and second edition. By this, we hope to reproduce the same impact as last years' editions and increase the number of submissions.


